(set-option :produce-models true)
;(set-option :produce-proofs true)
(set-option :model-compact false)
(set-option :produce-unsat-cores true)
(set-option :pull-nested-quantifiers true)
(set-option :mbqi true)

(declare-sort V-INN)    ; unV-INNerpreted 
(declare-sort E-INN)    ; unV-INNerpreted 
(declare-sort V-OUT)    ; unV-OUTerpreted 
(declare-sort E-OUT)    ; unV-OUTerpreted 

; Source and target model type declaration
(declare-fun PI (V-INN) Bool)
(declare-fun F1I (V-INN) Bool)
(declare-fun F2I (V-INN) Bool)
(declare-fun TI (V-INN) Bool)
(declare-fun RI (V-INN) Bool)
(declare-fun VI (V-INN) Bool)
(declare-fun non-activeI (V-INN V-INN E-INN) Bool)
(declare-fun activeI (V-INN V-INN E-INN) Bool)
(declare-fun startI (V-INN V-INN E-INN) Bool)
(declare-fun critI (V-INN V-INN E-INN) Bool)
(declare-fun checkI (V-INN V-INN E-INN) Bool)
(declare-fun setTurnI (V-INN V-INN E-INN) Bool)
(declare-fun PF2I (V-INN V-INN E-INN) Bool)
(declare-fun PF1I (V-INN V-INN E-INN) Bool)
(declare-fun TPI (V-INN V-INN E-INN) Bool)
(declare-fun F2RI (V-INN V-INN E-INN) Bool)
(declare-fun F1RI (V-INN V-INN E-INN) Bool)
(declare-fun TRI (V-INN V-INN E-INN) Bool)
(declare-fun NEI (V-INN V-INN E-INN) Bool)
(declare-fun PO (V-OUT) Bool)
(declare-fun F1O (V-OUT) Bool)
(declare-fun F2O (V-OUT) Bool)
(declare-fun TO (V-OUT) Bool)
(declare-fun RO (V-OUT) Bool)
(declare-fun VO (V-OUT) Bool)
(declare-fun non-activeO (V-OUT V-OUT E-OUT) Bool)
(declare-fun activeO (V-OUT V-OUT E-OUT) Bool)
(declare-fun startO (V-OUT V-OUT E-OUT) Bool)
(declare-fun critO (V-OUT V-OUT E-OUT) Bool)
(declare-fun checkO (V-OUT V-OUT E-OUT) Bool)
(declare-fun setTurnO (V-OUT V-OUT E-OUT) Bool)
(declare-fun PF2O (V-OUT V-OUT E-OUT) Bool)
(declare-fun PF1O (V-OUT V-OUT E-OUT) Bool)
(declare-fun TPO (V-OUT V-OUT E-OUT) Bool)
(declare-fun F2RO (V-OUT V-OUT E-OUT) Bool)
(declare-fun F1RO (V-OUT V-OUT E-OUT) Bool)
(declare-fun TRO (V-OUT V-OUT E-OUT) Bool)
(declare-fun NEO (V-OUT V-OUT E-OUT) Bool)
;Assistant functions
(define-fun NNullVI ((a V-INN)) Bool (or (PI a) (or (F1I a) (or (F2I a) (or (TI a) (RI a))))))
(define-fun NNullEI ((a V-INN) (b V-INN) (c E-INN)) Bool (or (non-activeI a b c) (or (activeI a b c) (or (startI a b c) (or (critI a b c) (checkI a b c))))))
(define-fun ValidVI ((a V-INN)) Bool (or (NNullVI a) (VI a)))
(define-fun ValidEI ((a V-INN) (b V-INN) (c E-INN)) Bool (or (NNullEI a b c) (NEI a b c)))
(define-fun NNullVO ((a V-OUT)) Bool (or (PO a) (or (F1O a) (or (F2O a) (or (TO a) (RO a))))))
(define-fun NNullEO ((a V-OUT) (b V-OUT) (c E-OUT)) Bool (or (non-activeO a b c) (or (activeO a b c) (or (startO a b c) (or (critO a b c) (checkO a b c))))))
(define-fun ValidVO ((a V-OUT)) Bool (or (NNullVO a) (VO a)))
(define-fun ValidEO ((a V-OUT) (b V-OUT) (c E-OUT)) Bool (or (NNullEO a b c) (NEO a b c)))

;Source and target model type constraint
;Each element in the instance could be typed by only one element in the metamodel
(assert (! (forall ((a V-INN)) (and (and (and (and (and (not (and (PI a) (or (or (or (or (F1I a) (F2I a)) (TI a)) (RI a)) (VI a)))) (not (and (F1I a) (or (or (or (or (PI a) (F2I a)) (TI a)) (RI a)) (VI a))))) (not (and (F2I a) (or (or (or (or (PI a) (F1I a)) (TI a)) (RI a)) (VI a))))) (not (and (TI a) (or (or (or (or (PI a) (F1I a)) (F2I a)) (RI a)) (VI a))))) (not (and (RI a) (or (or (or (or (PI a) (F1I a)) (F2I a)) (TI a)) (VI a))))) (not (and (VI a) (or (or (or (or (PI a) (F1I a)) (F2I a)) (TI a)) (RI a)))))) :named Source-node-incompatiable))
(assert (! (forall ((s V-INN) (t V-INN) (e E-INN)) (and (and (and (and (and (and (and (and (and (and (and (and (not (and (non-activeI s t e) (or (or (or (or (or (or (or (or (or (or (or (activeI s t e) (startI s t e)) (critI s t e)) (checkI s t e)) (setTurnI s t e)) (PF2I s t e)) (PF1I s t e)) (TPI s t e)) (F2RI s t e)) (F1RI s t e)) (TRI s t e)) (NEI s t e)))) (not (and (activeI s t e) (or (or (or (or (or (or (or (or (or (or (or (non-activeI s t e) (startI s t e)) (critI s t e)) (checkI s t e)) (setTurnI s t e)) (PF2I s t e)) (PF1I s t e)) (TPI s t e)) (F2RI s t e)) (F1RI s t e)) (TRI s t e)) (NEI s t e))))) (not (and (startI s t e) (or (or (or (or (or (or (or (or (or (or (or (non-activeI s t e) (activeI s t e)) (critI s t e)) (checkI s t e)) (setTurnI s t e)) (PF2I s t e)) (PF1I s t e)) (TPI s t e)) (F2RI s t e)) (F1RI s t e)) (TRI s t e)) (NEI s t e))))) (not (and (critI s t e) (or (or (or (or (or (or (or (or (or (or (or (non-activeI s t e) (activeI s t e)) (startI s t e)) (checkI s t e)) (setTurnI s t e)) (PF2I s t e)) (PF1I s t e)) (TPI s t e)) (F2RI s t e)) (F1RI s t e)) (TRI s t e)) (NEI s t e))))) (not (and (checkI s t e) (or (or (or (or (or (or (or (or (or (or (or (non-activeI s t e) (activeI s t e)) (startI s t e)) (critI s t e)) (setTurnI s t e)) (PF2I s t e)) (PF1I s t e)) (TPI s t e)) (F2RI s t e)) (F1RI s t e)) (TRI s t e)) (NEI s t e))))) (not (and (setTurnI s t e) (or (or (or (or (or (or (or (or (or (or (or (non-activeI s t e) (activeI s t e)) (startI s t e)) (critI s t e)) (checkI s t e)) (PF2I s t e)) (PF1I s t e)) (TPI s t e)) (F2RI s t e)) (F1RI s t e)) (TRI s t e)) (NEI s t e))))) (not (and (PF2I s t e) (or (or (or (or (or (or (or (or (or (or (or (non-activeI s t e) (activeI s t e)) (startI s t e)) (critI s t e)) (checkI s t e)) (setTurnI s t e)) (PF1I s t e)) (TPI s t e)) (F2RI s t e)) (F1RI s t e)) (TRI s t e)) (NEI s t e))))) (not (and (PF1I s t e) (or (or (or (or (or (or (or (or (or (or (or (non-activeI s t e) (activeI s t e)) (startI s t e)) (critI s t e)) (checkI s t e)) (setTurnI s t e)) (PF2I s t e)) (TPI s t e)) (F2RI s t e)) (F1RI s t e)) (TRI s t e)) (NEI s t e))))) (not (and (TPI s t e) (or (or (or (or (or (or (or (or (or (or (or (non-activeI s t e) (activeI s t e)) (startI s t e)) (critI s t e)) (checkI s t e)) (setTurnI s t e)) (PF2I s t e)) (PF1I s t e)) (F2RI s t e)) (F1RI s t e)) (TRI s t e)) (NEI s t e))))) (not (and (F2RI s t e) (or (or (or (or (or (or (or (or (or (or (or (non-activeI s t e) (activeI s t e)) (startI s t e)) (critI s t e)) (checkI s t e)) (setTurnI s t e)) (PF2I s t e)) (PF1I s t e)) (TPI s t e)) (F1RI s t e)) (TRI s t e)) (NEI s t e))))) (not (and (F1RI s t e) (or (or (or (or (or (or (or (or (or (or (or (non-activeI s t e) (activeI s t e)) (startI s t e)) (critI s t e)) (checkI s t e)) (setTurnI s t e)) (PF2I s t e)) (PF1I s t e)) (TPI s t e)) (F2RI s t e)) (TRI s t e)) (NEI s t e))))) (not (and (TRI s t e) (or (or (or (or (or (or (or (or (or (or (or (non-activeI s t e) (activeI s t e)) (startI s t e)) (critI s t e)) (checkI s t e)) (setTurnI s t e)) (PF2I s t e)) (PF1I s t e)) (TPI s t e)) (F2RI s t e)) (F1RI s t e)) (NEI s t e))))) (not (and (NEI s t e) (or (or (or (or (or (or (or (or (or (or (or (non-activeI s t e) (activeI s t e)) (startI s t e)) (critI s t e)) (checkI s t e)) (setTurnI s t e)) (PF2I s t e)) (PF1I s t e)) (TPI s t e)) (F2RI s t e)) (F1RI s t e)) (TRI s t e)))))) :named Source-edge-incompatiable))
(assert (! (forall ((a V-OUT)) (and (and (and (and (and (not (and (PO a) (or (or (or (or (F1O a) (F2O a)) (TO a)) (RO a)) (VO a)))) (not (and (F1O a) (or (or (or (or (PO a) (F2O a)) (TO a)) (RO a)) (VO a))))) (not (and (F2O a) (or (or (or (or (PO a) (F1O a)) (TO a)) (RO a)) (VO a))))) (not (and (TO a) (or (or (or (or (PO a) (F1O a)) (F2O a)) (RO a)) (VO a))))) (not (and (RO a) (or (or (or (or (PO a) (F1O a)) (F2O a)) (TO a)) (VO a))))) (not (and (VO a) (or (or (or (or (PO a) (F1O a)) (F2O a)) (TO a)) (RO a)))))) :named Target-node-incompatiable))
(assert (! (forall ((s V-OUT) (t V-OUT) (e E-OUT)) (and (and (and (and (and (and (and (and (and (and (and (and (not (and (non-activeO s t e) (or (or (or (or (or (or (or (or (or (or (or (activeO s t e) (startO s t e)) (critO s t e)) (checkO s t e)) (setTurnO s t e)) (PF2O s t e)) (PF1O s t e)) (TPO s t e)) (F2RO s t e)) (F1RO s t e)) (TRO s t e)) (NEO s t e)))) (not (and (activeO s t e) (or (or (or (or (or (or (or (or (or (or (or (non-activeO s t e) (startO s t e)) (critO s t e)) (checkO s t e)) (setTurnO s t e)) (PF2O s t e)) (PF1O s t e)) (TPO s t e)) (F2RO s t e)) (F1RO s t e)) (TRO s t e)) (NEO s t e))))) (not (and (startO s t e) (or (or (or (or (or (or (or (or (or (or (or (non-activeO s t e) (activeO s t e)) (critO s t e)) (checkO s t e)) (setTurnO s t e)) (PF2O s t e)) (PF1O s t e)) (TPO s t e)) (F2RO s t e)) (F1RO s t e)) (TRO s t e)) (NEO s t e))))) (not (and (critO s t e) (or (or (or (or (or (or (or (or (or (or (or (non-activeO s t e) (activeO s t e)) (startO s t e)) (checkO s t e)) (setTurnO s t e)) (PF2O s t e)) (PF1O s t e)) (TPO s t e)) (F2RO s t e)) (F1RO s t e)) (TRO s t e)) (NEO s t e))))) (not (and (checkO s t e) (or (or (or (or (or (or (or (or (or (or (or (non-activeO s t e) (activeO s t e)) (startO s t e)) (critO s t e)) (setTurnO s t e)) (PF2O s t e)) (PF1O s t e)) (TPO s t e)) (F2RO s t e)) (F1RO s t e)) (TRO s t e)) (NEO s t e))))) (not (and (setTurnO s t e) (or (or (or (or (or (or (or (or (or (or (or (non-activeO s t e) (activeO s t e)) (startO s t e)) (critO s t e)) (checkO s t e)) (PF2O s t e)) (PF1O s t e)) (TPO s t e)) (F2RO s t e)) (F1RO s t e)) (TRO s t e)) (NEO s t e))))) (not (and (PF2O s t e) (or (or (or (or (or (or (or (or (or (or (or (non-activeO s t e) (activeO s t e)) (startO s t e)) (critO s t e)) (checkO s t e)) (setTurnO s t e)) (PF1O s t e)) (TPO s t e)) (F2RO s t e)) (F1RO s t e)) (TRO s t e)) (NEO s t e))))) (not (and (PF1O s t e) (or (or (or (or (or (or (or (or (or (or (or (non-activeO s t e) (activeO s t e)) (startO s t e)) (critO s t e)) (checkO s t e)) (setTurnO s t e)) (PF2O s t e)) (TPO s t e)) (F2RO s t e)) (F1RO s t e)) (TRO s t e)) (NEO s t e))))) (not (and (TPO s t e) (or (or (or (or (or (or (or (or (or (or (or (non-activeO s t e) (activeO s t e)) (startO s t e)) (critO s t e)) (checkO s t e)) (setTurnO s t e)) (PF2O s t e)) (PF1O s t e)) (F2RO s t e)) (F1RO s t e)) (TRO s t e)) (NEO s t e))))) (not (and (F2RO s t e) (or (or (or (or (or (or (or (or (or (or (or (non-activeO s t e) (activeO s t e)) (startO s t e)) (critO s t e)) (checkO s t e)) (setTurnO s t e)) (PF2O s t e)) (PF1O s t e)) (TPO s t e)) (F1RO s t e)) (TRO s t e)) (NEO s t e))))) (not (and (F1RO s t e) (or (or (or (or (or (or (or (or (or (or (or (non-activeO s t e) (activeO s t e)) (startO s t e)) (critO s t e)) (checkO s t e)) (setTurnO s t e)) (PF2O s t e)) (PF1O s t e)) (TPO s t e)) (F2RO s t e)) (TRO s t e)) (NEO s t e))))) (not (and (TRO s t e) (or (or (or (or (or (or (or (or (or (or (or (non-activeO s t e) (activeO s t e)) (startO s t e)) (critO s t e)) (checkO s t e)) (setTurnO s t e)) (PF2O s t e)) (PF1O s t e)) (TPO s t e)) (F2RO s t e)) (F1RO s t e)) (NEO s t e))))) (not (and (NEO s t e) (or (or (or (or (or (or (or (or (or (or (or (non-activeO s t e) (activeO s t e)) (startO s t e)) (critO s t e)) (checkO s t e)) (setTurnO s t e)) (PF2O s t e)) (PF1O s t e)) (TPO s t e)) (F2RO s t e)) (F1RO s t e)) (TRO s t e)))))) :named Target-edge-incompatiable))

;Any NullEdge only comes and goes to those nodes
(assert (! (forall ((a V-INN) (b V-INN) (c E-INN)) (=> (NEI a b c)  (or (or (or (or (and (PI a) (PI b)) (and (PI a) (VI b))) (and (VI a) (RI b))) (and (VI a) (VI b))) (and (TI a) (PI b))))) :named Source-NullEdge-Source-Target))
(assert (! (forall ((a V-OUT) (b V-OUT) (c E-OUT)) (=> (NEO a b c)  (or (or (or (or (and (PO a) (PO b)) (and (PO a) (VO b))) (and (VO a) (RO b))) (and (VO a) (VO b))) (and (TO a) (PO b))))) :named Target-NullEdge-Source-Target))
(assert (! (forall ((a V-OUT) (b V-OUT) (c E-OUT) (d V-OUT) (e V-OUT) (f E-OUT)) (=> (and (NEO a b c) (NEO d e f)) (= c f))) :named only-one-NEO-exists))
(assert (! (forall ((a V-INN) (b V-INN) (c E-INN) (d V-INN) (e V-INN) (f E-INN)) (=> (and (NEI a b c) (NEI d e f)) (= c f))) :named only-one-NEI-exists))

;Any edge comes in or goes out an invalid node is invalid
(assert (! (forall ((a V-INN) (b V-INN) (c E-INN)) (=> (not (ValidVI a)) (and (not (ValidEI a b c)) (not (ValidEI b a c))))) :named source-untyped-node-edge-undefined))
(assert (! (forall ((a V-OUT) (b V-OUT) (c E-OUT)) (=> (not (ValidVO a)) (and (not (ValidEO a b c)) (not (ValidEO b a c))))) :named target-untyped-node-edge-undefined))

;Any edge comes in or goes out an null node is null
(assert (! (forall ((s V-INN) (t V-INN) (e E-INN)) (=> (VI s) (and (=> (ValidEI s t e) (NEI s t e)) (=> (ValidEI t s e) (NEI t s e))))) :named VI-null-incoming-null-outing))
(assert (! (forall ((s V-OUT) (t V-OUT) (e E-OUT)) (=> (VO s) (and (=> (ValidEO s t e) (NEO s t e)) (=> (ValidEO t s e) (NEO t s e))))) :named VO-null-incoming-null-outing))

;Source and target information of an edge in metamodel should well kept in the instance level
(assert (! (forall ((s V-INN) (t V-INN) (e E-INN)) (=> (non-activeI s t e) (and (PI s) (PI t)))) :named non-activeI-source-target))
(assert (! (forall ((s V-INN) (t V-INN) (e E-INN)) (=> (activeI s t e) (and (PI s) (PI t)))) :named activeI-source-target))
(assert (! (forall ((s V-INN) (t V-INN) (e E-INN)) (=> (startI s t e) (and (PI s) (PI t)))) :named startI-source-target))
(assert (! (forall ((s V-INN) (t V-INN) (e E-INN)) (=> (critI s t e) (and (PI s) (PI t)))) :named critI-source-target))
(assert (! (forall ((s V-INN) (t V-INN) (e E-INN)) (=> (checkI s t e) (and (PI s) (PI t)))) :named checkI-source-target))
(assert (! (forall ((s V-INN) (t V-INN) (e E-INN)) (=> (setTurnI s t e) (and (PI s) (PI t)))) :named setTurnI-source-target))
(assert (! (forall ((s V-INN) (t V-INN) (e E-INN)) (=> (PF2I s t e) (and (PI s) (F2I t)))) :named PF2I-source-target))
(assert (! (forall ((s V-INN) (t V-INN) (e E-INN)) (=> (PF1I s t e) (and (PI s) (F1I t)))) :named PF1I-source-target))
(assert (! (forall ((s V-INN) (t V-INN) (e E-INN)) (=> (TPI s t e) (and (TI s) (PI t)))) :named TPI-source-target))
(assert (! (forall ((s V-INN) (t V-INN) (e E-INN)) (=> (F2RI s t e) (and (F2I s) (RI t)))) :named F2RI-source-target))
(assert (! (forall ((s V-INN) (t V-INN) (e E-INN)) (=> (F1RI s t e) (and (F1I s) (RI t)))) :named F1RI-source-target))
(assert (! (forall ((s V-INN) (t V-INN) (e E-INN)) (=> (TRI s t e) (and (TI s) (RI t)))) :named TRI-source-target))


(assert (! (forall ((s V-OUT) (t V-OUT) (e E-OUT)) (=> (non-activeO s t e) (and (PO s) (PO t)))) :named non-activeO-source-target))
(assert (! (forall ((s V-OUT) (t V-OUT) (e E-OUT)) (=> (activeO s t e) (and (PO s) (PO t)))) :named activeO-source-target))
(assert (! (forall ((s V-OUT) (t V-OUT) (e E-OUT)) (=> (startO s t e) (and (PO s) (PO t)))) :named startO-source-target))
(assert (! (forall ((s V-OUT) (t V-OUT) (e E-OUT)) (=> (critO s t e) (and (PO s) (PO t)))) :named critO-source-target))
(assert (! (forall ((s V-OUT) (t V-OUT) (e E-OUT)) (=> (checkO s t e) (and (PO s) (PO t)))) :named checkO-source-target))
(assert (! (forall ((s V-OUT) (t V-OUT) (e E-OUT)) (=> (setTurnO s t e) (and (PO s) (PO t)))) :named setTurnO-source-target))
(assert (! (forall ((s V-OUT) (t V-OUT) (e E-OUT)) (=> (PF2O s t e) (and (PO s) (F2O t)))) :named PF2O-source-target))
(assert (! (forall ((s V-OUT) (t V-OUT) (e E-OUT)) (=> (PF1O s t e) (and (PO s) (F1O t)))) :named PF1O-source-target))
(assert (! (forall ((s V-OUT) (t V-OUT) (e E-OUT)) (=> (TPO s t e) (and (TO s) (PO t)))) :named TPO-source-target))
(assert (! (forall ((s V-OUT) (t V-OUT) (e E-OUT)) (=> (F2RO s t e) (and (F2O s) (RO t)))) :named F2RO-source-target))
(assert (! (forall ((s V-OUT) (t V-OUT) (e E-OUT)) (=> (F1RO s t e) (and (F1O s) (RO t)))) :named F1RO-source-target))
(assert (! (forall ((s V-OUT) (t V-OUT) (e E-OUT)) (=> (TRO s t e) (and (TO s) (RO t)))) :named TRO-source-target))



;If edge (s, t, e) is an valid edge, then other combination (s', t', e) are invalid
(assert (! (forall ((s V-INN) (t V-INN) (e E-INN)) (=> (NNullEI s t e) (forall ((s1 V-INN) (t1 V-INN)) (=> (not (and (= s s1) (= t t1))) (not (ValidEI s1 t1 e)))))) :named source-edge-exclusive))
(assert (! (forall ((s V-OUT) (t V-OUT) (e E-OUT)) (=> (NNullEO s t e) (forall ((s1 V-OUT) (t1 V-OUT)) (=> (not (and (= s s1) (= t t1))) (not (ValidEO s1 t1 e)))))) :named target-edge-exclusive))

;Only one Null Node exists in instance level
(assert (! (forall ((s V-INN) (t V-INN)) (or (= s t) (not (and (VI s) (VI t))))) :named Source-only-one-null-node-allowed))
(assert (! (forall ((s V-OUT) (t V-OUT)) (or (= s t) (not (and (VO s) (VO t))))) :named Target-only-one-null-node-allowed))
(assert (! (forall ((s V-INN) (t V-INN) (e E-INN) (e1 E-INN)) (or (= e e1) (not (and (NEI s t e) (NEI s t e1))))) :named Source-only-one-null-edge-allowed))
(assert (! (forall ((s V-OUT) (t V-OUT) (e E-OUT) (e1 E-OUT)) (or (= e e1) (not (and (NEO s t e) (NEO s t e1))))) :named Target-only-one-null-edge-allowed))

;encoding of Add and Del function
(declare-datatypes () ((InnTuple (inn-tuple (s V-INN) (t V-INN) (e E-INN)))))
(declare-datatypes () ((OutTuple (out-tuple (s V-OUT) (t V-OUT) (e E-OUT)))))
(declare-fun addV (V-OUT) V-INN)
(declare-fun delV (V-INN) V-OUT)
(declare-fun addE (V-OUT V-OUT E-OUT) InnTuple)
(declare-fun delE (V-INN V-INN E-INN) OutTuple)

;graph morphism
(assert (! (forall ((a V-INN) (b V-INN) (c E-INN) (d V-OUT) (e V-OUT) (f E-OUT)) (=> (and (ValidEO d e f) (= (addE d e f) (inn-tuple a b c))) (and (= (addV d) a) (= (addV e) b)))) :named add-graph-morphism))
(assert (! (forall ((a V-INN) (b V-INN) (c E-INN) (d V-OUT) (e V-OUT) (f E-OUT)) (=> (and (ValidEI a b c) (= (delE a b c) (out-tuple d e f))) (and (= (delV a) d) (= (delV b) e)))) :named del-graph-morphism))

;Invalid elements and Null elements are changed into Null elements
(assert (! (forall ((a V-INN) (b V-OUT)) (=> (and (or (not (ValidVI a)) (VI a)) (= (delV a) b)) (VO b))) :named Null-Inn-Or-Invalid-Node-Null-Out-Deled))
(assert (! (forall ((a V-OUT) (b V-INN)) (=> (and (or (not (ValidVO a)) (VO a)) (= (addV a) b)) (VI b))) :named Null-Out-Or-Invalid-Node-Null-Inn-Added))
(assert (! (forall ((a V-INN) (b V-INN) (c E-INN) (d V-OUT) (e V-OUT) (f E-OUT)) (=> (and (not (ValidEI a b c)) (= (delE a b c) (out-tuple d e f))) (and (= d e) (and (VO d) (NEO d e f))))) :named Invalid-Edge-Null-Out-Edge-Deled))
(assert (! (forall ((a V-OUT) (b V-OUT) (c E-OUT) (d V-INN) (e V-INN) (f E-INN)) (=> (and (not (ValidEO a b c)) (= (addE a b c) (inn-tuple d e f))) (and (= d e) (and (VI d) (NEI d e f))))) :named Invalid-Edge-Null-Inn-Edge-Added))
(assert (! (forall ((a V-OUT) (b V-OUT) (c E-OUT) (d V-INN) (e V-INN) (f E-INN)) (=> (and (NEO a b c) (= (addE a b c) (inn-tuple d e f))) (NEI d e f))) :named Null-Out-Edge-Null-Inn-Edge-Added))
(assert (! (forall ((a V-INN) (b V-INN) (c E-INN) (d V-OUT) (e V-OUT) (f E-OUT)) (=> (and (NEI a b c) (= (delE a b c) (out-tuple d e f))) (NEO d e f))) :named Null-Inn-Edge-Null-Out-Edge-Deled))

;Commond part for each transformation are well kept
(assert (! (forall ((a V-INN) (b V-OUT)) (=> (and (and (NNullVI a) (NNullVO b)) (= (delV a) b)) (= (addV b) a))) :named common-node-del-bi))
(assert (! (forall ((a V-INN) (b V-OUT)) (=> (and (and (NNullVI a) (NNullVO b)) (= (addV b) a)) (= (delV a) b))) :named common-node-add-bi))
(assert (! (forall ((a V-INN) (b V-INN) (c E-INN) (d V-OUT) (e V-OUT) (f E-OUT)) (=> (and (and (NNullEI a b c) (NNullEO d e f)) (= (delE a b c) (out-tuple d e f))) (= (addE d e f) (inn-tuple a b c)))) :named common-edge-del-bi))
(assert (! (forall ((a V-INN) (b V-INN) (c E-INN) (d V-OUT) (e V-OUT) (f E-OUT)) (=> (and (and (NNullEO d e f) (NNullEI a b c)) (= (addE d e f) (inn-tuple a b c))) (= (delE a b c) (out-tuple d e f)))) :named common-edge-add-bi))

;the type of commond elements are well kept
(assert (! (forall ((a V-INN) (b V-OUT)) (=> (and (and (NNullVI a) (NNullVO b)) (= (delV a) b))
 (and (and (and (and (and (=> (PI a) (PO b)) (=> (PO b) (PI a))) (and (=> (F1I a) (F1O b)) (=> (F1O b) (F1I a))))
 (and (=> (F2I a) (F2O b)) (=> (F2O b) (F2I a))))
 (and (=> (TI a) (TO b)) (=> (TO b) (TI a))))
 (and (=> (RI a) (RO b)) (=> (RO b) (RI a))))
)) :named type-del-kept))
(assert (! (forall ((a V-INN) (b V-OUT)) (=> (and (and (NNullVI a) (NNullVO b)) (= (addV b) a))
 (and (and (and (and (and (=> (PI a) (PO b)) (=> (PO b) (PI a))) (and (=> (F1I a) (F1O b)) (=> (F1O b) (F1I a))))
 (and (=> (F2I a) (F2O b)) (=> (F2O b) (F2I a))))
 (and (=> (TI a) (TO b)) (=> (TO b) (TI a))))
 (and (=> (RI a) (RO b)) (=> (RO b) (RI a))))
)) :named type-add-kept))
(assert (! (forall ((a V-INN) (b V-INN) (c E-INN) (d V-OUT) (e V-OUT) (f E-OUT)) (=> (and (and (NNullEI a b c) (NNullEO d e f)) (= (delE a b c) (out-tuple d e f)))
 (and (and (and (and (and (and (and (and (and (and (and (and (=> (non-activeI a b c) (non-activeO d e f)) (=> (non-activeO d e f) (non-activeI a b c))) (and (=> (activeI a b c) (activeO d e f)) (=> (activeO d e f) (activeI a b c))))
 (and (=> (startI a b c) (startO d e f)) (=> (startO d e f) (startI a b c))))
 (and (=> (critI a b c) (critO d e f)) (=> (critO d e f) (critI a b c))))
 (and (=> (checkI a b c) (checkO d e f)) (=> (checkO d e f) (checkI a b c))))
 (and (=> (setTurnI a b c) (setTurnO d e f)) (=> (setTurnO d e f) (setTurnI a b c))))
 (and (=> (PF2I a b c) (PF2O d e f)) (=> (PF2O d e f) (PF2I a b c))))
 (and (=> (PF1I a b c) (PF1O d e f)) (=> (PF1O d e f) (PF1I a b c))))
 (and (=> (TPI a b c) (TPO d e f)) (=> (TPO d e f) (TPI a b c))))
 (and (=> (F2RI a b c) (F2RO d e f)) (=> (F2RO d e f) (F2RI a b c))))
 (and (=> (F1RI a b c) (F1RO d e f)) (=> (F1RO d e f) (F1RI a b c))))
 (and (=> (TRI a b c) (TRO d e f)) (=> (TRO d e f) (TRI a b c))))
)) :named edge-type-del-kept))
(assert (! (forall ((a V-INN) (b V-INN) (c E-INN) (d V-OUT) (e V-OUT) (f E-OUT)) (=> (and (and (NNullEO d e f) (NNullEI a b c)) (= (addE d e f) (inn-tuple a b c)))
 (and (and (and (and (and (and (and (and (and (and (and (and (=> (non-activeI a b c) (non-activeO d e f)) (=> (non-activeO d e f) (non-activeI a b c))) (and (=> (activeI a b c) (activeO d e f)) (=> (activeO d e f) (activeI a b c))))
 (and (=> (startI a b c) (startO d e f)) (=> (startO d e f) (startI a b c))))
 (and (=> (critI a b c) (critO d e f)) (=> (critO d e f) (critI a b c))))
 (and (=> (checkI a b c) (checkO d e f)) (=> (checkO d e f) (checkI a b c))))
 (and (=> (setTurnI a b c) (setTurnO d e f)) (=> (setTurnO d e f) (setTurnI a b c))))
 (and (=> (PF2I a b c) (PF2O d e f)) (=> (PF2O d e f) (PF2I a b c))))
 (and (=> (PF1I a b c) (PF1O d e f)) (=> (PF1O d e f) (PF1I a b c))))
 (and (=> (TPI a b c) (TPO d e f)) (=> (TPO d e f) (TPI a b c))))
 (and (=> (F2RI a b c) (F2RO d e f)) (=> (F2RO d e f) (F2RI a b c))))
 (and (=> (F1RI a b c) (F1RO d e f)) (=> (F1RO d e f) (F1RI a b c))))
 (and (=> (TRI a b c) (TRO d e f)) (=> (TRO d e f) (TRI a b c))))
)) :named edge-type-add-kept))

;common elements are mapped injectively
(assert (! (forall ((a V-INN) (b V-OUT) (c V-OUT)) (=> (and (and (NNullVO b) (NNullVO c)) (and (= (addV b) a) (NNullVI a))) (or (= c b) (not (= (addV c) a))))) :named node-add-injective))
(assert (! (forall ((a V-INN) (b V-OUT) (c V-INN)) (=> (and (and (NNullVI a) (NNullVI c)) (and (= (delV a) b) (NNullVO b))) (or (= c a) (not (= (delV c) b))))) :named node-del-injective))
(assert (! (forall ((a V-INN) (b V-INN) (c E-INN) (d V-OUT) (e V-OUT) (f E-OUT) (h V-OUT) (i V-OUT) (j E-OUT)) (=> (and (and (NNullEO d e f) (NNullEO h i j)) (and (= (addE d e f) (inn-tuple a b c)) (NNullEI a b c))) (or (or (= d h) (or (= e i) (= f j))) (not (= (addE h i j) (inn-tuple a b c)))))) :named edge-add-injective))
(assert (! (forall ((a V-INN) (b V-INN) (c E-INN) (d V-OUT) (e V-OUT) (f E-OUT) (h V-INN) (i V-INN) (j E-INN)) (=> (and (and (NNullEI a b c) (NNullEI h i j)) (and (= (delE a b c) (out-tuple d e f)) (NNullEO d e f))) (or (or (= a h) (or (= b i) (= c j))) (not (= (delE h i j) (out-tuple d e f)))))) :named edge-del-injective))

;Each valid elements in the target model should hava a preimage for del
;Each valid elements in the source model should hava a preimage for add
(assert (! (forall ((a V-OUT)) (=> (NNullVO a) (exists ((b V-INN)) (and (NNullVI b) (= a (delV b)))))) :named del-surjective-for-NotNull-node-in-target))
(assert (! (forall ((a V-INN)) (=> (NNullVI a) (exists ((b V-OUT)) (and (NNullVO b) (= a (addV b)))))) :named add-surjective-for-NotNull-node-in-source))
(assert (! (forall ((a V-INN) (b V-INN) (c E-INN)) (=> (NNullEI a b c) (exists ((d V-OUT) (e V-OUT) (f E-OUT)) (and (NNullEO d e f) (= (addE d e f) (inn-tuple a b c)))))) :named add-surjective-for-NotNull-edge-in-source))
(assert (! (forall ((a V-OUT) (b V-OUT) (c E-OUT)) (=> (NNullEO a b c) (exists ((d V-INN) (e V-INN) (f E-INN)) (and (NNullEI d e f) (= (delE d e f) (out-tuple a b c)))))) :named del-surjective-for-NotNull-edge-in-target))

;Each invalid elements in the target model should hava no preimage for del
;Each invalid elements in the source model should hava no preimage for add
(assert (! (forall ((t V-OUT)) (=> (not (ValidVO t)) (not (exists ((s V-INN)) (= (delV s) t))))) :named no-invalid-node-in-source-has-pre-image-in-del))
(assert (! (forall ((s V-INN)) (=> (not (ValidVI s)) (not (exists ((t V-OUT)) (= (addV t) s))))) :named no-invalid-node-in-target-has-pre-image-in-add))
(assert (! (forall ((s V-OUT) (t V-OUT) (e E-OUT)) (=> (not (ValidEO s t e)) (not (exists ((a V-INN) (b V-INN) (c E-INN)) (= (delE a b c) (out-tuple s t e)))))) :named no-invalid-edge-in-source-has-pre-image-in-del))
(assert (! (forall ((a V-INN) (b V-INN) (c E-INN)) (=> (not (ValidEI a b c)) (not (exists ((s V-OUT) (t V-OUT) (e E-OUT)) (= (addE s t e) (inn-tuple a b c)))))) :named no-invalid-edge-in-target-has-pre-image-in-add))

(declare-datatypes () ((RuleID idsetFlag idsetTurn1 idsetTurn2 identer idexit)))
(declare-fun delVID (V-INN RuleID) Bool)
(declare-fun addVID (V-OUT RuleID) Bool)
(declare-fun delEID (V-INN V-INN E-INN RuleID) Bool)
(declare-fun addEID (V-OUT V-OUT E-OUT RuleID) Bool)
(assert (! (forall ((a V-INN) (id RuleID)) (=> (or (not (ValidVI a)) (or (VI a) (and (NNullVI a) (exists ((b V-OUT)) (and (NNullVO b) (= (delV a) b)))))) (not (delVID a id)))) :named del-node-id-false))
(assert (! (forall ((a V-OUT) (id RuleID)) (=> (or (not (ValidVO a)) (or (VO a) (and (NNullVO a) (exists ((b V-INN)) (and (NNullVI b) (= (addV a) b)))))) (not (addVID a id)))) :named add-node-id-false))
(assert (! (forall ((a V-INN) (b V-INN) (c E-INN) (id RuleID)) (=> (or (not (ValidEI a b c)) (or (NEI a b c) (and (NNullEI a b c) (exists ((d V-OUT) (e V-OUT) (f E-OUT)) (and (NNullEO d e f) (= (delE a b c) (out-tuple d e f))))))) (not (delEID a b c id)))) :named del-edge-id-false))
(assert (! (forall ((a V-OUT) (b V-OUT) (c E-OUT) (id RuleID)) (=> (or (not (ValidEO a b c)) (or (NEO a b c) (and (NNullEO a b c) (exists ((d V-INN) (e V-INN) (f E-INN)) (and (NNullEI d e f) (= (addE a b c) (inn-tuple d e f))))))) (not (addEID a b c id)))) :named add-edge-id-false))
(assert (! (forall ((a V-INN)) (=> (and (NNullVI a) (exists ((b V-OUT)) (and (VO b) (= (delV a) b)))) (exists ((id RuleID)) (delVID a id)))) :named del-node-id-true))
(assert (! (forall ((a V-OUT)) (=> (and (NNullVO a) (exists ((b V-INN)) (and (VI b) (= (addV a) b)))) (exists ((id RuleID)) (addVID a id)))) :named add-node-id-true))
(assert (! (forall ((a V-INN) (b V-INN) (c E-INN)) (=> (and (NNullEI a b c) (exists ((d V-OUT) (e V-OUT) (f E-OUT)) (and (NEO d e f) (= (delE a b c) (out-tuple d e f))))) (exists ((id RuleID)) (delEID a b c id)))) :named del-edge-id-true))
(assert (! (forall ((a V-OUT) (b V-OUT) (c E-OUT)) (=> (and (NNullEO a b c) (exists ((d V-INN) (e V-INN) (f E-INN)) (and (NEI d e f) (= (addE a b c) (inn-tuple d e f))))) (exists ((id RuleID)) (addEID a b c id)))) :named add-edge-id-true))
(assert (! (forall ((a V-INN) (id RuleID)) (=> (not (delVID a id)) (or (not (ValidVI a)) (or (VI a) (and (NNullVI a) (exists ((b V-OUT)) (and (NNullVO b) (= (delV a) b)))))))) :named del-node-id-false-domain))
(assert (! (forall ((a V-OUT) (id RuleID)) (=> (not (addVID a id)) (or (not (ValidVO a)) (or (VO a) (and (NNullVO a) (exists ((b V-INN)) (and (NNullVI b) (= (addV a) b)))))))) :named add-node-id-false-domain))
(assert (! (forall ((a V-INN) (b V-INN) (c E-INN) (id RuleID)) (=> (not (delEID a b c id)) (or (not (ValidEI a b c)) (or (NEI a b c) (and (NNullEI a b c) (exists ((d V-OUT) (e V-OUT) (f E-OUT)) (and (NNullEO d e f) (= (delE a b c) (out-tuple d e f))))))))) :named del-edge-id-false-domain))
(assert (! (forall ((a V-OUT) (b V-OUT) (c E-OUT) (id RuleID)) (=> (not (addEID a b c id)) (or (not (ValidEO a b c)) (or (NEO a b c) (and (NNullEO a b c) (exists ((d V-INN) (e V-INN) (f E-INN)) (and (NNullEI d e f) (= (addE a b c) (inn-tuple d e f))))))))) :named add-edge-id-false-domain))
(assert (! (forall ((a V-INN)) (=> (exists ((id RuleID)) (delVID a id)) (and (NNullVI a) (exists ((b V-OUT)) (and (VO b) (= (delV a) b)))))) :named del-node-id-true-domain))
(assert (! (forall ((a V-OUT)) (=> (exists ((id RuleID)) (addVID a id)) (and (NNullVO a) (exists ((b V-INN)) (and (VI b) (= (addV a) b)))))) :named add-node-id-true-domain))
(assert (! (forall ((a V-INN) (b V-INN) (c E-INN)) (=> (exists ((id RuleID)) (delEID a b c id)) (and (NNullEI a b c) (exists ((d V-OUT) (e V-OUT) (f E-OUT)) (and (NEO d e f) (= (delE a b c) (out-tuple d e f))))))) :named del-edge-id-true-domain))
(assert (! (forall ((a V-OUT) (b V-OUT) (c E-OUT)) (=> (exists ((id RuleID)) (addEID a b c id)) (and (NNullEO a b c) (exists ((d V-INN) (e V-INN) (f E-INN)) (and (NEI d e f) (= (addE a b c) (inn-tuple d e f))))))) :named add-edge-id-true-domain))
(assert (! (forall ((a V-INN) (b V-INN) (c E-INN) (id RuleID)) (=> (delVID a id) (and (=> (NNullEI a b c) (delEID a b c id)) (=> (NNullEI b a c) (delEID b a c id))))) :named id-node-del-edge-del))
(assert (! (forall ((a V-OUT) (b V-OUT) (c E-OUT) (id RuleID)) (=> (addVID a id) (and (=> (NNullEO a b c) (addEID a b c id)) (=> (NNullEO b a c) (addEID b a c id))))) :named id-node-add-edge-add))
(assert (! (forall ((a V-INN)) (and (and (and (and (not (and (delVID a idsetFlag) (or (or (or (delVID a idsetTurn1) (delVID a idsetTurn2)) (delVID a identer)) (delVID a idexit)))) (not (and (delVID a idsetTurn1) (or (or (or (delVID a idsetFlag) (delVID a idsetTurn2)) (delVID a identer)) (delVID a idexit))))) (not (and (delVID a idsetTurn2) (or (or (or (delVID a idsetFlag) (delVID a idsetTurn1)) (delVID a identer)) (delVID a idexit))))) (not (and (delVID a identer) (or (or (or (delVID a idsetFlag) (delVID a idsetTurn1)) (delVID a idsetTurn2)) (delVID a idexit))))) (not (and (delVID a idexit) (or (or (or (delVID a idsetFlag) (delVID a idsetTurn1)) (delVID a idsetTurn2)) (delVID a identer)))))) :named Del-node-only-once))
(assert (! (forall ((a V-OUT)) (and (and (and (and (not (and (addVID a idsetFlag) (or (or (or (addVID a idsetTurn1) (addVID a idsetTurn2)) (addVID a identer)) (addVID a idexit)))) (not (and (addVID a idsetTurn1) (or (or (or (addVID a idsetFlag) (addVID a idsetTurn2)) (addVID a identer)) (addVID a idexit))))) (not (and (addVID a idsetTurn2) (or (or (or (addVID a idsetFlag) (addVID a idsetTurn1)) (addVID a identer)) (addVID a idexit))))) (not (and (addVID a identer) (or (or (or (addVID a idsetFlag) (addVID a idsetTurn1)) (addVID a idsetTurn2)) (addVID a idexit))))) (not (and (addVID a idexit) (or (or (or (addVID a idsetFlag) (addVID a idsetTurn1)) (addVID a idsetTurn2)) (addVID a identer)))))) :named Add-node-only-once))
(assert (! (forall ((a V-INN) (b V-INN) (c E-INN)) (and (and (and (and (not (and (delEID a b c idsetFlag) (or (or (or (delEID a b c idsetTurn1) (delEID a b c idsetTurn2)) (delEID a b c identer)) (delEID a b c idexit)))) (not (and (delEID a b c idsetTurn1) (or (or (or (delEID a b c idsetFlag) (delEID a b c idsetTurn2)) (delEID a b c identer)) (delEID a b c idexit))))) (not (and (delEID a b c idsetTurn2) (or (or (or (delEID a b c idsetFlag) (delEID a b c idsetTurn1)) (delEID a b c identer)) (delEID a b c idexit))))) (not (and (delEID a b c identer) (or (or (or (delEID a b c idsetFlag) (delEID a b c idsetTurn1)) (delEID a b c idsetTurn2)) (delEID a b c idexit))))) (not (and (delEID a b c idexit) (or (or (or (delEID a b c idsetFlag) (delEID a b c idsetTurn1)) (delEID a b c idsetTurn2)) (delEID a b c identer)))))) :named Del-edge-only-once))
(assert (! (forall ((a V-OUT) (b V-OUT) (c E-OUT)) (and (and (and (and (not (and (addEID a b c idsetFlag) (or (or (or (addEID a b c idsetTurn1) (addEID a b c idsetTurn2)) (addEID a b c identer)) (addEID a b c idexit)))) (not (and (addEID a b c idsetTurn1) (or (or (or (addEID a b c idsetFlag) (addEID a b c idsetTurn2)) (addEID a b c identer)) (addEID a b c idexit))))) (not (and (addEID a b c idsetTurn2) (or (or (or (addEID a b c idsetFlag) (addEID a b c idsetTurn1)) (addEID a b c identer)) (addEID a b c idexit))))) (not (and (addEID a b c identer) (or (or (or (addEID a b c idsetFlag) (addEID a b c idsetTurn1)) (addEID a b c idsetTurn2)) (addEID a b c idexit))))) (not (and (addEID a b c idexit) (or (or (or (addEID a b c idsetFlag) (addEID a b c idsetTurn1)) (addEID a b c idsetTurn2)) (addEID a b c identer)))))) :named Add-edge-only-once))
;Rule setFlag
(assert (! (forall ( (ei1 E-INN) (ei2 E-INN) (ni1 V-INN) (ni2 V-INN) (ni-2 V-INN) (ei-2 E-INN)) 
(=> (and (and (and (and (and (and (and (and (non-activeI ni1 ni1 ei1) (startI ni1 ni1 ei2)) (PI ni1)) (RI ni2)) (VI ni-2)) (NEI ni1 ni1 ei-2)) (NEI ni1 ni1 ei-2)) (NEI ni1 ni-2 ei-2)) (NEI ni-2 ni2 ei-2)) 
(or (exists ( (eo1 E-OUT) (eo2 E-OUT) (no1 V-OUT) (no2 V-OUT) (no-2 V-OUT) (eo-2 E-OUT)) 
(and (and (and (and (and (and (and (and (and (non-activeO no1 no1 eo1) (startO no1 no1 eo2)) (PO no1)) (RO no2)) (VO no-2)) (NEO no1 no1 eo-2)) (NEO no1 no1 eo-2)) (NEO no1 no-2 eo-2)) (NEO no-2 no2 eo-2))
 (and (and (and (and (and (and (and (and (= (out-tuple no1 no1 eo1) (delE ni1 ni1 ei1)) (= (out-tuple no1 no1 eo2) (delE ni1 ni1 ei2))) (= no1 (delV ni1))) (= no2 (delV ni2))) (= no-2 (delV ni-2))) (= (out-tuple no1 no1 eo-2) (delE ni1 ni1 ei-2))) (= (out-tuple no1 no1 eo-2) (delE ni1 ni1 ei-2))) (= (out-tuple no1 no-2 eo-2) (delE ni1 ni-2 ei-2))) (= (out-tuple no-2 no2 eo-2) (delE ni-2 ni2 ei-2))))) 
(exists ( (no3 V-OUT) (eo3 E-OUT) (eo4 E-OUT) (eo5 E-OUT) (eo6 E-OUT) (no1 V-OUT) (no2 V-OUT) (eo-1 E-OUT)) 
(and (and (and (and (and (and (and (and (and (F1O no3) (activeO no1 no1 eo3)) (setTurnO no1 no1 eo4)) (PF1O no1 no3 eo5)) (F1RO no3 no2 eo6)) (PO no1)) (RO no2)) (NEO no1 no1 eo-1)) (NEO no1 no1 eo-1)) 
(and (and (and (and (and (and (and (and (and (and (and (= (out-tuple no1 no1 eo-1) (delE ni1 ni1 ei1)) (= (out-tuple no1 no1 eo-1) (delE ni1 ni1 ei2))) (= no1 (delV ni1))) (= no2 (delV ni2))) (= ni1 (addV no1))) (= ni2 (addV no2))) (= ni-2 (addV no3))) (= (inn-tuple ni1 ni1 ei-2) (addE no1 no1 eo3))) (= (inn-tuple ni1 ni1 ei-2) (addE no1 no1 eo4))) (= (inn-tuple ni1 ni-2 ei-2) (addE no1 no3 eo5))) (= (inn-tuple ni-2 ni2 ei-2) (addE no3 no2 eo6)))
 (and (and (and (and (and (and (delEID ni1 ni1 ei1 idsetFlag) (delEID ni1 ni1 ei2 idsetFlag)) (addVID no3 idsetFlag)) (addEID no1 no1 eo3 idsetFlag)) (addEID no1 no1 eo4 idsetFlag)) (addEID no1 no3 eo5 idsetFlag)) (addEID no3 no2 eo6 idsetFlag)))))))) :named rule-setFlag))
;Rule setTurn1
(assert (! (forall ( (ei3 E-INN) (ei4 E-INN) (ni1 V-INN) (ni2 V-INN) (ni3 V-INN) (ni4 V-INN) (ei1 E-INN) (ei2 E-INN) (ei-2 E-INN)) 
(=> (and (and (and (and (and (and (and (and (and (TPI ni3 ni1 ei3) (setTurnI ni2 ni2 ei4)) (PI ni1)) (PI ni2)) (TI ni3)) (RI ni4)) (non-activeI ni1 ni1 ei1)) (TRI ni3 ni4 ei2)) (NEI ni2 ni2 ei-2)) (NEI ni3 ni2 ei-2)) 
(or (exists ( (eo3 E-OUT) (eo4 E-OUT) (no1 V-OUT) (no2 V-OUT) (no3 V-OUT) (no4 V-OUT) (eo1 E-OUT) (eo2 E-OUT) (eo-2 E-OUT)) 
(and (and (and (and (and (and (and (and (and (and (TPO no3 no1 eo3) (setTurnO no2 no2 eo4)) (PO no1)) (PO no2)) (TO no3)) (RO no4)) (non-activeO no1 no1 eo1)) (TRO no3 no4 eo2)) (NEO no2 no2 eo-2)) (NEO no3 no2 eo-2))
 (and (and (and (and (and (and (and (and (and (= (out-tuple no3 no1 eo3) (delE ni3 ni1 ei3)) (= (out-tuple no2 no2 eo4) (delE ni2 ni2 ei4))) (= no1 (delV ni1))) (= no2 (delV ni2))) (= no3 (delV ni3))) (= no4 (delV ni4))) (= (out-tuple no1 no1 eo1) (delE ni1 ni1 ei1))) (= (out-tuple no3 no4 eo2) (delE ni3 ni4 ei2))) (= (out-tuple no2 no2 eo-2) (delE ni2 ni2 ei-2))) (= (out-tuple no3 no2 eo-2) (delE ni3 ni2 ei-2))))) 
(exists ( (eo5 E-OUT) (eo6 E-OUT) (no1 V-OUT) (no2 V-OUT) (no3 V-OUT) (no4 V-OUT) (eo1 E-OUT) (eo2 E-OUT) (eo-1 E-OUT)) 
(and (and (and (and (and (and (and (and (and (and (checkO no2 no2 eo5) (TPO no3 no2 eo6)) (PO no1)) (PO no2)) (TO no3)) (RO no4)) (non-activeO no1 no1 eo1)) (TRO no3 no4 eo2)) (NEO no3 no1 eo-1)) (NEO no2 no2 eo-1)) 
(and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= (out-tuple no3 no1 eo-1) (delE ni3 ni1 ei3)) (= (out-tuple no2 no2 eo-1) (delE ni2 ni2 ei4))) (= no1 (delV ni1))) (= no2 (delV ni2))) (= no3 (delV ni3))) (= no4 (delV ni4))) (= ni1 (addV no1))) (= ni2 (addV no2))) (= ni3 (addV no3))) (= ni4 (addV no4))) (= (out-tuple no1 no1 eo1) (delE ni1 ni1 ei1))) (= (out-tuple no3 no4 eo2) (delE ni3 ni4 ei2))) (= (inn-tuple ni1 ni1 ei1) (addE no1 no1 eo1))) (= (inn-tuple ni3 ni4 ei2) (addE no3 no4 eo2))) (= (inn-tuple ni2 ni2 ei-2) (addE no2 no2 eo5))) (= (inn-tuple ni3 ni2 ei-2) (addE no3 no2 eo6)))
 (and (and (and (delEID ni3 ni1 ei3 idsetTurn1) (delEID ni2 ni2 ei4 idsetTurn1)) (addEID no2 no2 eo5 idsetTurn1)) (addEID no3 no2 eo6 idsetTurn1)))))))) :named rule-setTurn1))
;Rule setTurn2
(assert (! (forall ( (ei3 E-INN) (ni1 V-INN) (ni2 V-INN) (ni3 V-INN) (ei1 E-INN) (ei2 E-INN) (ei-2 E-INN)) 
(=> (and (and (and (and (and (and (setTurnI ni1 ni1 ei3) (PI ni1)) (TI ni2)) (RI ni3)) (TPI ni2 ni1 ei1)) (TRI ni2 ni3 ei2)) (NEI ni1 ni1 ei-2)) 
(or (exists ( (eo3 E-OUT) (no1 V-OUT) (no2 V-OUT) (no3 V-OUT) (eo1 E-OUT) (eo2 E-OUT) (eo-2 E-OUT)) 
(and (and (and (and (and (and (and (setTurnO no1 no1 eo3) (PO no1)) (TO no2)) (RO no3)) (TPO no2 no1 eo1)) (TRO no2 no3 eo2)) (NEO no1 no1 eo-2))
 (and (and (and (and (and (and (= (out-tuple no1 no1 eo3) (delE ni1 ni1 ei3)) (= no1 (delV ni1))) (= no2 (delV ni2))) (= no3 (delV ni3))) (= (out-tuple no2 no1 eo1) (delE ni2 ni1 ei1))) (= (out-tuple no2 no3 eo2) (delE ni2 ni3 ei2))) (= (out-tuple no1 no1 eo-2) (delE ni1 ni1 ei-2))))) 
(exists ( (eo4 E-OUT) (no1 V-OUT) (no2 V-OUT) (no3 V-OUT) (eo1 E-OUT) (eo2 E-OUT) (eo-1 E-OUT)) 
(and (and (and (and (and (and (and (checkO no1 no1 eo4) (PO no1)) (TO no2)) (RO no3)) (TPO no2 no1 eo1)) (TRO no2 no3 eo2)) (NEO no1 no1 eo-1)) 
(and (and (and (and (and (and (and (and (and (and (and (and (= (out-tuple no1 no1 eo-1) (delE ni1 ni1 ei3)) (= no1 (delV ni1))) (= no2 (delV ni2))) (= no3 (delV ni3))) (= ni1 (addV no1))) (= ni2 (addV no2))) (= ni3 (addV no3))) (= (out-tuple no2 no1 eo1) (delE ni2 ni1 ei1))) (= (out-tuple no2 no3 eo2) (delE ni2 ni3 ei2))) (= (inn-tuple ni2 ni1 ei1) (addE no2 no1 eo1))) (= (inn-tuple ni2 ni3 ei2) (addE no2 no3 eo2))) (= (inn-tuple ni1 ni1 ei-2) (addE no1 no1 eo4)))
 (and (delEID ni1 ni1 ei3 idsetTurn2) (addEID no1 no1 eo4 idsetTurn2)))))))) :named rule-setTurn2))
;Rule enter
(assert (! (forall ( (ni4 V-INN) (ei3 E-INN) (ei4 E-INN) (ei5 E-INN) (ni1 V-INN) (ni2 V-INN) (ni3 V-INN) (ei1 E-INN) (ei2 E-INN) (ni-2 V-INN) (ei-2 E-INN)) 
(=> (and (and (and (and (and (and (and (and (and (and (and (and (F1I ni4) (checkI ni1 ni1 ei3)) (PF1I ni1 ni4 ei4)) (F1RI ni4 ni3 ei5)) (PI ni1)) (TI ni2)) (RI ni3)) (TPI ni2 ni1 ei1)) (TRI ni2 ni3 ei2)) (VI ni-2)) (NEI ni1 ni1 ei-2)) (NEI ni1 ni-2 ei-2)) (NEI ni-2 ni3 ei-2)) 
(or (exists ( (no4 V-OUT) (eo3 E-OUT) (eo4 E-OUT) (eo5 E-OUT) (no1 V-OUT) (no2 V-OUT) (no3 V-OUT) (eo1 E-OUT) (eo2 E-OUT) (no-2 V-OUT) (eo-2 E-OUT)) 
(and (and (and (and (and (and (and (and (and (and (and (and (and (F1O no4) (checkO no1 no1 eo3)) (PF1O no1 no4 eo4)) (F1RO no4 no3 eo5)) (PO no1)) (TO no2)) (RO no3)) (TPO no2 no1 eo1)) (TRO no2 no3 eo2)) (VO no-2)) (NEO no1 no1 eo-2)) (NEO no1 no-2 eo-2)) (NEO no-2 no3 eo-2))
 (and (and (and (and (and (and (and (and (and (and (and (and (= no4 (delV ni4)) (= (out-tuple no1 no1 eo3) (delE ni1 ni1 ei3))) (= (out-tuple no1 no4 eo4) (delE ni1 ni4 ei4))) (= (out-tuple no4 no3 eo5) (delE ni4 ni3 ei5))) (= no1 (delV ni1))) (= no2 (delV ni2))) (= no3 (delV ni3))) (= (out-tuple no2 no1 eo1) (delE ni2 ni1 ei1))) (= (out-tuple no2 no3 eo2) (delE ni2 ni3 ei2))) (= no-2 (delV ni-2))) (= (out-tuple no1 no1 eo-2) (delE ni1 ni1 ei-2))) (= (out-tuple no1 no-2 eo-2) (delE ni1 ni-2 ei-2))) (= (out-tuple no-2 no3 eo-2) (delE ni-2 ni3 ei-2))))) 
(exists ( (no5 V-OUT) (eo6 E-OUT) (eo7 E-OUT) (eo8 E-OUT) (no1 V-OUT) (no2 V-OUT) (no3 V-OUT) (eo1 E-OUT) (eo2 E-OUT) (no-1 V-OUT) (eo-1 E-OUT)) 
(and (and (and (and (and (and (and (and (and (and (and (and (and (F2O no5) (critO no1 no1 eo6)) (PF2O no1 no5 eo7)) (F2RO no5 no3 eo8)) (PO no1)) (TO no2)) (RO no3)) (TPO no2 no1 eo1)) (TRO no2 no3 eo2)) (VO no-1)) (NEO no1 no1 eo-1)) (NEO no1 no-1 eo-1)) (NEO no-1 no3 eo-1)) 
(and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= no-1 (delV ni4)) (= (out-tuple no1 no1 eo-1) (delE ni1 ni1 ei3))) (= (out-tuple no1 no-1 eo-1) (delE ni1 ni4 ei4))) (= (out-tuple no-1 no3 eo-1) (delE ni4 ni3 ei5))) (= no1 (delV ni1))) (= no2 (delV ni2))) (= no3 (delV ni3))) (= ni1 (addV no1))) (= ni2 (addV no2))) (= ni3 (addV no3))) (= (out-tuple no2 no1 eo1) (delE ni2 ni1 ei1))) (= (out-tuple no2 no3 eo2) (delE ni2 ni3 ei2))) (= (inn-tuple ni2 ni1 ei1) (addE no2 no1 eo1))) (= (inn-tuple ni2 ni3 ei2) (addE no2 no3 eo2))) (= ni-2 (addV no5))) (= (inn-tuple ni1 ni1 ei-2) (addE no1 no1 eo6))) (= (inn-tuple ni1 ni-2 ei-2) (addE no1 no5 eo7))) (= (inn-tuple ni-2 ni3 ei-2) (addE no5 no3 eo8)))
 (and (and (and (and (and (and (and (delVID ni4 identer) (delEID ni1 ni1 ei3 identer)) (delEID ni1 ni4 ei4 identer)) (delEID ni4 ni3 ei5 identer)) (addVID no5 identer)) (addEID no1 no1 eo6 identer)) (addEID no1 no5 eo7 identer)) (addEID no5 no3 eo8 identer)))))))) :named rule-enter))
;Rule exit
(assert (! (forall ( (ni3 V-INN) (ei1 E-INN) (ei2 E-INN) (ei3 E-INN) (ei4 E-INN) (ni1 V-INN) (ni2 V-INN) (ei-2 E-INN)) 
(=> (and (and (and (and (and (and (and (and (F2I ni3) (activeI ni1 ni1 ei1)) (critI ni1 ni1 ei2)) (PF2I ni1 ni3 ei3)) (F2RI ni3 ni2 ei4)) (PI ni1)) (RI ni2)) (NEI ni1 ni1 ei-2)) (NEI ni1 ni1 ei-2)) 
(or (exists ( (no3 V-OUT) (eo1 E-OUT) (eo2 E-OUT) (eo3 E-OUT) (eo4 E-OUT) (no1 V-OUT) (no2 V-OUT) (eo-2 E-OUT)) 
(and (and (and (and (and (and (and (and (and (F2O no3) (activeO no1 no1 eo1)) (critO no1 no1 eo2)) (PF2O no1 no3 eo3)) (F2RO no3 no2 eo4)) (PO no1)) (RO no2)) (NEO no1 no1 eo-2)) (NEO no1 no1 eo-2))
 (and (and (and (and (and (and (and (and (= no3 (delV ni3)) (= (out-tuple no1 no1 eo1) (delE ni1 ni1 ei1))) (= (out-tuple no1 no1 eo2) (delE ni1 ni1 ei2))) (= (out-tuple no1 no3 eo3) (delE ni1 ni3 ei3))) (= (out-tuple no3 no2 eo4) (delE ni3 ni2 ei4))) (= no1 (delV ni1))) (= no2 (delV ni2))) (= (out-tuple no1 no1 eo-2) (delE ni1 ni1 ei-2))) (= (out-tuple no1 no1 eo-2) (delE ni1 ni1 ei-2))))) 
(exists ( (eo5 E-OUT) (eo6 E-OUT) (no1 V-OUT) (no2 V-OUT) (no-1 V-OUT) (eo-1 E-OUT)) 
(and (and (and (and (and (and (and (and (and (non-activeO no1 no1 eo5) (startO no1 no1 eo6)) (PO no1)) (RO no2)) (VO no-1)) (NEO no1 no1 eo-1)) (NEO no1 no1 eo-1)) (NEO no1 no-1 eo-1)) (NEO no-1 no2 eo-1)) 
(and (and (and (and (and (and (and (and (and (and (and (= no-1 (delV ni3)) (= (out-tuple no1 no1 eo-1) (delE ni1 ni1 ei1))) (= (out-tuple no1 no1 eo-1) (delE ni1 ni1 ei2))) (= (out-tuple no1 no-1 eo-1) (delE ni1 ni3 ei3))) (= (out-tuple no-1 no2 eo-1) (delE ni3 ni2 ei4))) (= no1 (delV ni1))) (= no2 (delV ni2))) (= ni1 (addV no1))) (= ni2 (addV no2))) (= (inn-tuple ni1 ni1 ei-2) (addE no1 no1 eo5))) (= (inn-tuple ni1 ni1 ei-2) (addE no1 no1 eo6)))
 (and (and (and (and (and (and (delVID ni3 idexit) (delEID ni1 ni1 ei1 idexit)) (delEID ni1 ni1 ei2 idexit)) (delEID ni1 ni3 ei3 idexit)) (delEID ni3 ni2 ei4 idexit)) (addEID no1 no1 eo5 idexit)) (addEID no1 no1 eo6 idexit)))))))) :named rule-exit))

(assert (! (or (or (or (exists ((a1 V-INN) (b1 V-OUT)) (=> (and (NNullVI a1) (= b1 (delV a1))) (VO b1))) 
(exists ((a2 V-OUT) (b2 V-INN)) (=> (and (NNullVO a2) (= b2 (addV a2))) (VI b2)))) 
(exists ((a3 V-INN) (b3 V-INN) (c3 E-INN) (d3 V-OUT) (e3 V-OUT) (f3 E-OUT)) (=> (and (NNullEI a3 b3 c3) (= (out-tuple d3 e3 f3) (delE a3 b3 c3))) (NEO d3 e3 f3)))) 
(exists ((a4 V-INN) (b4 V-INN) (c4 E-INN) (d4 V-OUT) (e4 V-OUT) (f4 E-OUT)) (=> (and (NNullEO d4 e4 f4) (= (inn-tuple a4 b4 c4) (addE d4 e4 f4))) (NEI a4 b4 c4)))) :named at-least-one-edge-node-is-added-or-deled))

(assert (!  (or (or (or (or
 (exists ( (ei_01 E-INN) (ei_02 E-INN) (ni_01 V-INN) (ni_02 V-INN) (ni_0-2 V-INN) (ei_0-2 E-INN)) 
 (and (and (and (and (and (and (and (and (non-activeI ni_01 ni_01 ei_01) (startI ni_01 ni_01 ei_02)) (PI ni_01)) (RI ni_02)) (VI ni_0-2)) (NEI ni_01 ni_01 ei_0-2)) (NEI ni_01 ni_01 ei_0-2)) (NEI ni_01 ni_0-2 ei_0-2)) (NEI ni_0-2 ni_02 ei_0-2)))
 (exists ( (ei_13 E-INN) (ei_14 E-INN) (ni_11 V-INN) (ni_12 V-INN) (ni_13 V-INN) (ni_14 V-INN) (ei_11 E-INN) (ei_12 E-INN) (ei_1-2 E-INN)) 
 (and (and (and (and (and (and (and (and (and (TPI ni_13 ni_11 ei_13) (setTurnI ni_12 ni_12 ei_14)) (PI ni_11)) (PI ni_12)) (TI ni_13)) (RI ni_14)) (non-activeI ni_11 ni_11 ei_11)) (TRI ni_13 ni_14 ei_12)) (NEI ni_12 ni_12 ei_1-2)) (NEI ni_13 ni_12 ei_1-2))))
 (exists ( (ei_23 E-INN) (ni_21 V-INN) (ni_22 V-INN) (ni_23 V-INN) (ei_21 E-INN) (ei_22 E-INN) (ei_2-2 E-INN)) 
 (and (and (and (and (and (and (setTurnI ni_21 ni_21 ei_23) (PI ni_21)) (TI ni_22)) (RI ni_23)) (TPI ni_22 ni_21 ei_21)) (TRI ni_22 ni_23 ei_22)) (NEI ni_21 ni_21 ei_2-2))))
 (exists ( (ni_34 V-INN) (ei_33 E-INN) (ei_34 E-INN) (ei_35 E-INN) (ni_31 V-INN) (ni_32 V-INN) (ni_33 V-INN) (ei_31 E-INN) (ei_32 E-INN) (ni_3-2 V-INN) (ei_3-2 E-INN)) 
 (and (and (and (and (and (and (and (and (and (and (and (and (F1I ni_34) (checkI ni_31 ni_31 ei_33)) (PF1I ni_31 ni_34 ei_34)) (F1RI ni_34 ni_33 ei_35)) (PI ni_31)) (TI ni_32)) (RI ni_33)) (TPI ni_32 ni_31 ei_31)) (TRI ni_32 ni_33 ei_32)) (VI ni_3-2)) (NEI ni_31 ni_31 ei_3-2)) (NEI ni_31 ni_3-2 ei_3-2)) (NEI ni_3-2 ni_33 ei_3-2))))
 (exists ( (ni_43 V-INN) (ei_41 E-INN) (ei_42 E-INN) (ei_43 E-INN) (ei_44 E-INN) (ni_41 V-INN) (ni_42 V-INN) (ei_4-2 E-INN)) 
 (and (and (and (and (and (and (and (and (F2I ni_43) (activeI ni_41 ni_41 ei_41)) (critI ni_41 ni_41 ei_42)) (PF2I ni_41 ni_43 ei_43)) (F2RI ni_43 ni_42 ei_44)) (PI ni_41)) (RI ni_42)) (NEI ni_41 ni_41 ei_4-2)) (NEI ni_41 ni_41 ei_4-2)))) :named source-model-should-match-at-least-one-rule))
(assert (! (forall ((s V-INN) (t V-INN) (e E-INN)) (=> (non-activeI s t e) (= s t))) :named non-activeI-reflexive))
(assert (! (forall ((s V-INN) (t V-INN) (e E-INN)) (=> (activeI s t e) (= s t))) :named activeI-reflexive))
(assert (! (forall ((s V-INN) (t V-INN) (e E-INN)) (=> (startI s t e) (= s t))) :named startI-reflexive))
(assert (! (forall ((s V-INN) (t V-INN) (e E-INN)) (=> (critI s t e) (= s t))) :named critI-reflexive))
(assert (! (forall ((s V-INN) (t V-INN) (e E-INN)) (=> (checkI s t e) (= s t))) :named checkI-reflexive))
(assert (! (forall ((s V-INN) (t V-INN) (e E-INN)) (=> (setTurnI s t e) (= s t))) :named setTurnI-reflexive))
(assert (! (forall ((a V-INN) (b V-INN)) (or (not (and (TI a) (TI b))) (= a b))) :named unique-TI))
(assert (! (forall ((a V-INN) (b V-INN)) (or (not (and (RI a) (RI b))) (= a b))) :named unique-RI))
(assert (! (exists ((a V-INN)) (TI a)) :named exist-TI))
(assert (! (exists ((a V-INN)) (RI a)) :named exist-RI))
(assert (! (exists ((a V-INN)) (PI a)) :named exist-PI))
(assert (! (exists ((s V-INN) (t V-INN) (e E-INN)) (TPI s t e)) :named exist-edge-TPI))
(assert (! (forall ((s V-INN)) (=> (PI s)  (or (exists ((t0 V-INN) (e0 E-INN)) (non-activeI s t0 e0)) (exists ((t1 V-INN) (e1 E-INN)) (activeI s t1 e1))))) :named exist-one-of-non-activeI-activeI-edges))
(assert (! (forall ((s V-INN)) (=> (PI s)  (or (or (or (exists ((t0 V-INN) (e0 E-INN)) (startI s t0 e0)) (exists ((t1 V-INN) (e1 E-INN)) (critI s t1 e1))) (exists ((t2 V-INN) (e2 E-INN)) (checkI s t2 e2))) (exists ((t3 V-INN) (e3 E-INN)) (setTurnI s t3 e3))))) :named exist-one-of-startI-critI-checkI-setTurnI-edges))
(assert (! (forall ((s V-INN)) (=> (PI s)  (and (not (and (exists ((b0 V-INN) (c0 E-INN)) (non-activeI s b0 c0)) (exists ((b0-1 V-INN) (c0-1 E-INN)) (activeI s b0-1 c0-1)))) (not (and (exists ((b1 V-INN) (c1 E-INN)) (activeI s b1 c1)) (exists ((b1-0 V-INN) (c1-0 E-INN)) (non-activeI s b1-0 c1-0))))))) :named non-activeI-activeI-incompatiable))
(assert (! (forall ((s V-INN)) (=> (PI s)  (and (and (and (not (and (exists ((b0 V-INN) (c0 E-INN)) (startI s b0 c0)) (or (or (exists ((b0-1 V-INN) (c0-1 E-INN)) (critI s b0-1 c0-1)) (exists ((b0-2 V-INN) (c0-2 E-INN)) (checkI s b0-2 c0-2))) (exists ((b0-3 V-INN) (c0-3 E-INN)) (setTurnI s b0-3 c0-3))))) (not (and (exists ((b1 V-INN) (c1 E-INN)) (critI s b1 c1)) (or (or (exists ((b1-0 V-INN) (c1-0 E-INN)) (startI s b1-0 c1-0)) (exists ((b1-2 V-INN) (c1-2 E-INN)) (checkI s b1-2 c1-2))) (exists ((b1-3 V-INN) (c1-3 E-INN)) (setTurnI s b1-3 c1-3)))))) (not (and (exists ((b2 V-INN) (c2 E-INN)) (checkI s b2 c2)) (or (or (exists ((b2-0 V-INN) (c2-0 E-INN)) (startI s b2-0 c2-0)) (exists ((b2-1 V-INN) (c2-1 E-INN)) (critI s b2-1 c2-1))) (exists ((b2-3 V-INN) (c2-3 E-INN)) (setTurnI s b2-3 c2-3)))))) (not (and (exists ((b3 V-INN) (c3 E-INN)) (setTurnI s b3 c3)) (or (or (exists ((b3-0 V-INN) (c3-0 E-INN)) (startI s b3-0 c3-0)) (exists ((b3-1 V-INN) (c3-1 E-INN)) (critI s b3-1 c3-1))) (exists ((b3-2 V-INN) (c3-2 E-INN)) (checkI s b3-2 c3-2)))))))) :named startI-critI-checkI-setTurnI-incompatiable))
(assert (! (forall ((s1 V-INN) (s2 V-INN) (t V-INN) (e1 E-INN) (e2 E-INN)) (=> (and (PF2I s1 t e1) (PF2I s2 t e2)) (and (= s1 s2) (= e1 e2)))) :named injective-PF2I))
(assert (! (forall ((s1 V-INN) (s2 V-INN) (t V-INN) (e1 E-INN) (e2 E-INN)) (=> (and (PF1I s1 t e1) (PF1I s2 t e2)) (and (= s1 s2) (= e1 e2)))) :named injective-PF1I))
(assert (! (forall ((s1 V-INN) (s2 V-INN) (t V-INN) (e1 E-INN) (e2 E-INN)) (=> (and (TRI s1 t e1) (TRI s2 t e2)) (and (= s1 s2) (= e1 e2)))) :named injective-TRI))
(assert (! (forall ((s1 V-INN) (s2 V-INN) (t V-INN) (e1 E-INN) (e2 E-INN)) (=> (and (TPI s1 t e1) (TPI s2 t e2)) (and (= s1 s2) (= e1 e2)))) :named injective-TPI))
(assert (! (forall ((s V-INN) (t1 V-INN) (t2 V-INN) (e1 E-INN) (e2 E-INN)) (=> (and (non-activeI s t1 e1) (non-activeI s t2 e2)) (and (= t1 t2) (= e1 e2)))) :named multi-0-1-non-activeI))
(assert (! (forall ((s V-INN) (t1 V-INN) (t2 V-INN) (e1 E-INN) (e2 E-INN)) (=> (and (activeI s t1 e1) (activeI s t2 e2)) (and (= t1 t2) (= e1 e2)))) :named multi-0-1-activeI))
(assert (! (forall ((s V-INN) (t1 V-INN) (t2 V-INN) (e1 E-INN) (e2 E-INN)) (=> (and (startI s t1 e1) (startI s t2 e2)) (and (= t1 t2) (= e1 e2)))) :named multi-0-1-startI))
(assert (! (forall ((s V-INN) (t1 V-INN) (t2 V-INN) (e1 E-INN) (e2 E-INN)) (=> (and (critI s t1 e1) (critI s t2 e2)) (and (= t1 t2) (= e1 e2)))) :named multi-0-1-critI))
(assert (! (forall ((s V-INN) (t1 V-INN) (t2 V-INN) (e1 E-INN) (e2 E-INN)) (=> (and (checkI s t1 e1) (checkI s t2 e2)) (and (= t1 t2) (= e1 e2)))) :named multi-0-1-checkI))
(assert (! (forall ((s V-INN) (t1 V-INN) (t2 V-INN) (e1 E-INN) (e2 E-INN)) (=> (and (setTurnI s t1 e1) (setTurnI s t2 e2)) (and (= t1 t2) (= e1 e2)))) :named multi-0-1-setTurnI))
(assert (! (forall ((s V-INN) (t1 V-INN) (t2 V-INN) (e1 E-INN) (e2 E-INN)) (=> (and (PF2I s t1 e1) (PF2I s t2 e2)) (and (= t1 t2) (= e1 e2)))) :named multi-0-1-PF2I))
(assert (! (forall ((s V-INN) (t1 V-INN) (t2 V-INN) (e1 E-INN) (e2 E-INN)) (=> (and (PF1I s t1 e1) (PF1I s t2 e2)) (and (= t1 t2) (= e1 e2)))) :named multi-0-1-PF1I))
(assert (! (forall ((s V-INN) (t1 V-INN) (t2 V-INN) (e1 E-INN) (e2 E-INN)) (=> (and (F1RI s t1 e1) (F1RI s t2 e2)) (and (= t1 t2) (= e1 e2)))) :named multi-0-1-F1RI))
(assert (! (forall ((s V-INN) (t1 V-INN) (t2 V-INN) (e1 E-INN) (e2 E-INN)) (=> (and (F2RI s t1 e1) (F2RI s t2 e2)) (and (= t1 t2) (= e1 e2)))) :named multi-0-1-F2RI))
(assert (! (forall ((s V-INN) (t1 V-INN) (t2 V-INN) (e1 E-INN) (e2 E-INN)) (=> (and (TPI s t1 e1) (TPI s t2 e2)) (and (= t1 t2) (= e1 e2)))) :named multi-0-1-TPI))
(assert (! (forall ((t V-INN)) (=> (F2I t) (exists ((s V-INN) (e E-INN)) (PF2I s t e)))) :named surjective-PF2I))
(assert (! (forall ((t V-INN)) (=> (F1I t) (exists ((s V-INN) (e E-INN)) (PF1I s t e)))) :named surjective-PF1I))
(assert (! (forall ((t V-INN)) (=> (RI t) (exists ((s V-INN) (e E-INN)) (TRI s t e)))) :named surjective-TRI))
(assert (! (forall ((s V-INN)) (=> (PI s) (not (exists ((t1 V-INN) (e1 E-INN) (t2 V-INN) (e2 E-INN)) (and (F1I t1) (and (F2I t2) (and (PF1I s t1 e1) (PF2I s t2 e2)))))))) :named xand-PF1-PF2I))
(assert (! (forall ((s V-INN)) (=> (PI s) (not (exists ((t1 V-INN) (e1 E-INN) (t2 V-INN) (e2 E-INN)) (and (PI t1) (and (PI t2) (and (non-activeI s t1 e1) (checkI s t2 e2)))))))) :named xand-non-active-checkI))
(assert (! (forall ((s V-INN)) (=> (PI s) (not (exists ((t1 V-INN) (e1 E-INN) (t2 V-INN) (e2 E-INN)) (and (PI t1) (and (PI t2) (and (non-activeI s t1 e1) (setTurnI s t2 e2)))))))) :named xand-non-active-setTurnI))
(assert (! (forall ((s V-INN)) (=> (PI s) (not (exists ((t1 V-INN) (e1 E-INN) (t2 V-INN) (e2 E-INN)) (and (PI t1) (and (PI t2) (and (non-activeI s t1 e1) (critI s t2 e2)))))))) :named xand-non-active-critI))
(assert (! (forall ((s V-INN)) (=> (PI s) (not (exists ((t1 V-INN) (e1 E-INN) (t2 V-INN) (e2 E-INN)) (and (PI t1) (and (PI t2) (and (activeI s t1 e1) (startI s t2 e2)))))))) :named xand-active-startI))
;(assert (! (not (exists ((a V-OUT)) (PO a))) :named exist-PO))
;(assert (! (not (exists ((a V-OUT)) (RO a))) :named exist-RO))
;(assert (! (not (exists ((a V-OUT)) (TO a))) :named exist-TO))
;(assert (! (not (forall ((a V-OUT) (b V-OUT)) (or (not (and (TO a) (TO b))) (= a b)))) :named unique-TO))
;(assert (! (not (forall ((a V-OUT) (b V-OUT)) (or (not (and (RO a) (RO b))) (= a b)))) :named unique-RO))
;(assert (! (not (forall ((s V-OUT)) (=> (PO s)  (or (exists ((t0 V-OUT) (e0 E-OUT)) (non-activeO s t0 e0)) (exists ((t1 V-OUT) (e1 E-OUT)) (activeO s t1 e1)))))) :named exist-one-of-non-activeO-activeO-edges))
;(assert (! (not (forall ((s V-OUT)) (=> (PO s)  (or (or (or (exists ((t0 V-OUT) (e0 E-OUT)) (startO s t0 e0)) (exists ((t1 V-OUT) (e1 E-OUT)) (critO s t1 e1))) (exists ((t2 V-OUT) (e2 E-OUT)) (checkO s t2 e2))) (exists ((t3 V-OUT) (e3 E-OUT)) (setTurnO s t3 e3)))))) :named exist-one-of-startO-critO-checkO-setTurnO-edges))
(assert (! (not (forall ((s V-OUT)) (=> (PO s)  (and (not (and (exists ((b0 V-OUT) (c0 E-OUT)) (non-activeO s b0 c0)) (exists ((b0-1 V-OUT) (c0-1 E-OUT)) (activeO s b0-1 c0-1)))) (not (and (exists ((b1 V-OUT) (c1 E-OUT)) (activeO s b1 c1)) (exists ((b1-0 V-OUT) (c1-0 E-OUT)) (non-activeO s b1-0 c1-0)))))))) :named non-activeO-activeO-incompatiable))
;(assert (! (not (forall ((s V-OUT)) (=> (PO s)  (and (and (and (not (and (exists ((b0 V-OUT) (c0 E-OUT)) (startO s b0 c0)) (or (or (exists ((b0-1 V-OUT) (c0-1 E-OUT)) (critO s b0-1 c0-1)) (exists ((b0-2 V-OUT) (c0-2 E-OUT)) (checkO s b0-2 c0-2))) (exists ((b0-3 V-OUT) (c0-3 E-OUT)) (setTurnO s b0-3 c0-3))))) (not (and (exists ((b1 V-OUT) (c1 E-OUT)) (critO s b1 c1)) (or (or (exists ((b1-0 V-OUT) (c1-0 E-OUT)) (startO s b1-0 c1-0)) (exists ((b1-2 V-OUT) (c1-2 E-OUT)) (checkO s b1-2 c1-2))) (exists ((b1-3 V-OUT) (c1-3 E-OUT)) (setTurnO s b1-3 c1-3)))))) (not (and (exists ((b2 V-OUT) (c2 E-OUT)) (checkO s b2 c2)) (or (or (exists ((b2-0 V-OUT) (c2-0 E-OUT)) (startO s b2-0 c2-0)) (exists ((b2-1 V-OUT) (c2-1 E-OUT)) (critO s b2-1 c2-1))) (exists ((b2-3 V-OUT) (c2-3 E-OUT)) (setTurnO s b2-3 c2-3)))))) (not (and (exists ((b3 V-OUT) (c3 E-OUT)) (setTurnO s b3 c3)) (or (or (exists ((b3-0 V-OUT) (c3-0 E-OUT)) (startO s b3-0 c3-0)) (exists ((b3-1 V-OUT) (c3-1 E-OUT)) (critO s b3-1 c3-1))) (exists ((b3-2 V-OUT) (c3-2 E-OUT)) (checkO s b3-2 c3-2))))))))) :named startO-critO-checkO-setTurnO-incompatiable))
;(assert (! (not (forall ((s V-OUT) (t V-OUT) (e E-OUT)) (=> (non-activeO s t e) (= s t)))) :named non-activeO-reflexive))
;(assert (! (not (forall ((s V-OUT) (t V-OUT) (e E-OUT)) (=> (activeO s t e) (= s t)))) :named activeO-reflexive))
;(assert (! (not (forall ((s V-OUT) (t V-OUT) (e E-OUT)) (=> (startO s t e) (= s t)))) :named startO-reflexive))
;(assert (! (not (forall ((s V-OUT) (t V-OUT) (e E-OUT)) (=> (critO s t e) (= s t)))) :named critO-reflexive))
;(assert (! (not (forall ((s V-OUT) (t V-OUT) (e E-OUT)) (=> (checkO s t e) (= s t)))) :named checkO-reflexive))
;(assert (! (not (forall ((s V-OUT) (t V-OUT) (e E-OUT)) (=> (setTurnO s t e) (= s t)))) :named setTurnO-reflexive))
;(assert (! (not (forall ((s1 V-OUT) (s2 V-OUT) (t V-OUT) (e1 E-OUT) (e2 E-OUT)) (=> (and (PF2O s1 t e1) (PF2O s2 t e2)) (and (= s1 s2) (= e1 e2))))) :named injective-PF2O))
;(assert (! (not (forall ((s1 V-OUT) (s2 V-OUT) (t V-OUT) (e1 E-OUT) (e2 E-OUT)) (=> (and (PF1O s1 t e1) (PF1O s2 t e2)) (and (= s1 s2) (= e1 e2))))) :named injective-PF1O))
;(assert (! (not (forall ((t V-OUT)) (=> (F2O t) (exists ((s V-OUT) (e E-OUT)) (PF2O s t e))))) :named surjective-PF2O))
;(assert (! (not (forall ((t V-OUT)) (=> (F1O t) (exists ((s V-OUT) (e E-OUT)) (PF1O s t e))))) :named surjective-PF1O))
;(assert (! (not (forall ((s V-OUT)) (=> (PO s) (not (exists ((t1 V-OUT) (e1 E-OUT) (t2 V-OUT) (e2 E-OUT)) (and (F1O t1) (and (F2O t2) (and (PF1O s t1 e1) (PF2O s t2 e2))))))))) :named xand-PF1-PF2O))
;(assert (! (forall ((p V-INN) (t V-INN) (f V-INN) (tp E-INN) (pf E-INN)) (=> (and (PI p) (and (TI t) (and (F2I f) (and (critI p p pf) (and (PF2I p f pf) (TPI t p tp))))))
; (not (exists ((p1 V-INN) (t1 V-INN) (f1 V-INN) (tp1 E-INN) (pf1 E-INN)) (and (not (= p p1)) (and (PI p1) (and (TI t1) (and (F2I f1) (and (critI p1 p1 pf1) (and (PF2I p1 f1 pf1) (TPI t1 p1 tp1))))))))))) :named access-exclusive-inn))
;(assert (! (not (forall ((p V-OUT) (t V-OUT) (f V-OUT) (tp E-OUT) (pf E-OUT)) (=> (and (PO p) (and (TO t) (and (F2O f) (and (critO p p pf) (and (PF2O p f pf) (TPO t p tp))))))
; (not (exists ((p1 V-OUT) (t1 V-OUT) (f1 V-OUT) (tp1 E-OUT) (pf1 E-OUT)) (and (not (= p p1)) (and (PO p1) (and (TO t1) (and (F2O f1) (and (critO p1 p1 pf1) (and (PF2O p1 f1 pf1) (TPO t1 p1 tp1)))))))))))) :named access-exclusive-out))
(check-sat)
(get-unsat-core)
(exit)
